Tute - Completed (Week 10)

1. Overloading
2. Subtyping
- 2.1. Coercions and Subtyping
- 2.2. Constructor variance
3. LCR Conditions
4. Session Types

1. Overloading

Consider the following file in Haskell:

class Compare a where
  cmp :: a -> a -> Bool

instance Compare Int where
  cmp x y = x <= y

instance (Compare a) => Compare [a] where
  cmp xs ys = and (zipWith cmp xs ys)

group  :: (Compare a) => [a] -> [[a]]
group []     = []
group (x:xs) = let (ys, zs) = span (cmp x) xs
                in (x:ys) : group zs

How would the type checker translate this code to remove the type classes?

type CompareDict a = (a -> a -> Bool)

intCompareDict :: CompareDict Int
intCompareDict x y = x <= y

listCompareDict :: CompareDict a -> CompareDict [a]
listCompareDict cmp xs ys = and (zipWith cmp xs ys)

group  :: CompareDict a -> [a] -> [[a]]
group cmp []     =  []
group cmp (x:xs) = let (ys, zs) = span (cmp x) xs
                    in (x:ys) : group cmp zs

2. Subtyping

2.1. Coercions and Subtyping

You are given the type Rectangle, parameterised by its height and width, and the type Square parameterised by the length of one of its sides. Neither type is mutable.

a. Which type is the subtype, which type is the supertype?

b. Give a subtype/supertype ordering of the following set of function types: Rectangle -> Rectangle, Rectangle -> Square, Square -> Rectangle, Square -> Square.

c. Define a data type Square and a data type Rectangle in Haskell. Then define a coercion function from elements of the subclass to elements of the superclass.

d. Show that the ordering you have given in the previous question is correct by defining coercion functions for each pair of types in a subtyping relationship in part (b).

a. Square is a subtype of Rectangle.

b. Rectangle -> Square is a subtype of Rectangle -> Rectangle and Square -> Square, which are both subtypes of Square -> Rectangle.

data Square = Square Int
data Rectangle = Rect Int Int

coerce :: Square -> Rectangle
coerce (Square w) = Rect w w

rs2rr :: (Rectangle -> Square) -> (Rectangle -> Rectangle)
rs2rr f = coerce . f

rs2ss :: (Rectangle -> Square) -> (Square -> Square)
rs2ss f = f . coerce

rr2sr :: (Rectangle -> Rectangle) -> (Square -> Rectangle)
rr2sr f = f . coerce

ss2sr :: (Square -> Square) -> (Square -> Rectangle)
ss2sr f = coerce . f

2.2. Constructor variance

List some examples of a covariant, contravariant and invariant type constructor.

A function's argument is contravariant. A function's return type is covariant. A data type like Endo below is invariant:

data Endo a = E (a -> a)

3. LCR Conditions

Consider the following two processes, each manipulating a shared variable \(x\), which starts out at \(0\).

Thread 1: \(x := x + 1; x:= x - 1;\)

Thread 2: \(x := x \times 2\)

a) What are the possible final values of \(x\) assuming each statement is executed atomically?

\(x\) is either zero or one.

b) Rewrite the above program into one where each statement obeys the limited critical reference restriction. What are the possible final values now?

Thread 1: \(\textbf{var}\ t; t := x; x := t + 1; t := x; x := t - 1;\)

Thread 2: \(\textbf{var}\ u; u := x; x := u \times 2\)

This allows the final write of thread 2 to happen well after the read of thread 2. Thus, a final result of \(x = 2\) or \(x = -1\) is now also possible.

c) How could locks be used in your answer to (b) to ensure that only the final results from part (a) are possible?

Each formerly-atomic statement must now be protected by a shared lock \(\ell\):

Thread 1: \(\begin{array}{l}\textbf{var}\ t; \mathbf{take}(\ell); t := x; x := t + 1; \mathbf{release}(\ell);\\ \mathbf{take}(\ell); t := x; x := t - 1; \mathbf{release}(\ell);\end{array}\)

Thread 2: \(\textbf{var}\ u; \mathbf{take}(\ell); u := x; x := u \times 2; \mathbf{release}(\ell);\)

4. Session Types

Using the session-typed process calculus introduced in the lecture, specify the process and type for a server that first takes the name of a product for sale, then provides a choice between two services:

Quote: output a price of type Price, then do nothing.
Sell: input payment details of type CardNo, output a receipt of type Receipt, then do nothing.

a) Define the types (i) Quote and (ii) Sell in terms of Price, CardNo, Receipt.

(i) Quote = Price ⨂ 1
(ii) Sell = CardNo ⅋ (Receipt ⨂ 1)

b) Assume we have processes give_price |- Γ,y:Price that transmits a Price along channel y and complete_sale |- Γ,y:CardNo,z:Receipt that accepts a CardNo on channel y then sends a Receipt on channel z. (You can leave their typing derivations unexpanded.)

Specify processes (i) quote of type Quote and (ii) sell of type Sell and show their typing derivations.

(i) quote := x[y].(give_price | x[].0) |- Γ,x:Quote

                              -------------- 1
give_price |- Γ,y:Price       x[].0 |- Δ,x:1
------------------------------------------- ⨂ 
x[y].(give_price | x[].0) |- Γ,Δ,x:Price ⨂ 1

(ii) x(y).x[z].(complete_sale | x[].0) |- x:Sell

                                               -------------- 1
     complete_sale |- Γ,y:CardNo,z:Receipt     x[].0 |- Δ,x:1
   ---------------------------------------------------------- ⨂ 
   x[z].(complete_sale | x[].0) |- Γ,Δ,y:CardNo,x:Receipt ⨂ 1
----------------------------------------------------------------- ⅋
x(y).x[z].(complete_sale | x[].0) |- Γ,Δ,x:CardNo ⅋ (Receipt ⨂ 1)

Note, it is not essential that the complete_sale has type dual(CardNo) rather than CardNo just because it is the receiver. It only matters that the processes on corresponding sides of the channel have types that are dual to each other. So it's fine for complete_sale to have type CardNo for y as long as the process on the other side of y has for it some type Blah = dual(CardNo).

c) Suppose the names of products for sale have type Name. Now specify the process and derive the type of the entire server. (You can leave quote, sell and their typing derivations unexpanded.)

server := x(w).x.case(quote, sell)) =
x(w).x.case((x[y].(give_price | x[].0)) | (x(y).x[z].(complete_sale | x[].0)))
|- x:Name ⅋ (Quote & Sell)

 quote |- w:Name,x:Quote     sell |- w:Name,x:Sell
 ------------------------------------------------- &
    x.case(quote, sell) |- w:Name,x:Quote & Sell
--------------------------------------------------- ⅋
x(w).x.case(quote, sell) |- x:Name ⅋ (Quote & Sell)

d) (i) Specify a process and type of a client seeking a quote from this server. You can specify the types as duals of the types above.

(ii) Show the typing derivation for the part that chooses to get the quote. You can leave get_price and its typing derivation unexpanded.

(i) We must choose types that are dual to that of the server. Suppose put_name sends a dual(Name) on channel w and get_price receives a dual(Price) on channel y. Then the following process will be able to be composed with the server according to the Cut rule.

First, let get_quote := x[inl].x(y).x().get_price. Then,

client := x[w].(put_name | get_quote)
|-
dual(Name) ⨂ (dual(Quote) ⨁ dual(Sell))

(ii) Note that dual(Quote) = dual(Price ⨂ 1) = dual(Price) ⅋ ⊥.

The typing derivation for get_quote is as follows:

            get_price |- y:dual(Price)
        ---------------------------------- ⊥
        x().get_price |- y:dual(Price),x:⊥
      --------------------------------------- ⅋ 
      x(y).x().get_price |- x:dual(Price) ⅋ ⊥
----------------------------------------------------- ⨁ 
x[inl].x(y).x().get_price |- dual(Quote) ⨁ dual(Sell)

e) Show the reduction of the process formed by parallel composition of the above client process with the server process.

ch x. (client | server)
== (unfolding client, server)
ch x. ((x[w].(put_name | get_quote)) | x(w).x.case(quote, sell))
==> (β⊗⅋)
ch w. (put_name | ch x. (get_quote | x.case(quote, sell)))
== (unfolding get_quote)
ch w. (put_name | ch x. (x[inl].x(y).x().get_price | x.case(quote, sell)))
==> (β⊕&1)
ch w. (put_name | ch x. (x(y).x().get_price | quote))
== (unfolding quote)
ch w. (put_name | ch x. (x(y).x().get_price | x[y].(give_price | x[].0)))
== (Swap)
ch w. (put_name | ch x. (x[y].(give_price | x[].0) | x(y).x().get_price))
==> (β⊗⅋)
ch w. (put_name | ch y. (give_price | ch x. (x[].0 | x().get_price)))
==> (β1⊥)
ch w. (put_name | ch y. (give_price | get_price)))